home *** CD-ROM | disk | FTP | other *** search
/ NetNews Offline 2 / NetNews Offline Volume 2.iso / news / comp / lang / c-part1 / 5310 < prev    next >
Encoding:
Internet Message Format  |  1996-08-05  |  3.0 KB
  1. Path: howland.reston.ans.net!psinntp!psinntp!psinntp!psinntp!www!www!not-for-mail
  2. From: cdh@www.oracorp.com (Douglas Harper)
  3. Newsgroups: comp.lang.c
  4. Subject: Re: Loop Invariant
  5. Date: 9 Feb 1996 16:52:08 -0500
  6. Organization: Odyssey Research Associates, Inc., Ithaca NY
  7. Sender: cdh@oracorp.com
  8. Message-ID: <4fgfm8$eeb@www.oracorp.com>
  9. NNTP-Posting-Host: www.oracorp.com
  10.  
  11.  
  12. Jonas J. Schlein  (schlein@gl.umbc.edu) writes:
  13. >Jason Klinke <jklinke@uvaix.uvic.ca> wrote:
  14. >|> I'm having difficulty coming up with a loop invariant that I can prove, for
  15. >|> the following code which computes the sum of the integers in the array 
  16. >|> A[0..n-1] :
  17. >|> 
  18. >|> -----------
  19. >|> sum = 0;
  20. >|> for (i = 0; i < n; i++)
  21. >|>     sum = sum + A[i];
  22. >|> -----------
  23. >|> 
  24. >|> Any help with this invariant and its proof is appreciated.
  25. >
  26. >Do it by induction...Verify that it works for the sum of the integers in
  27. >am empty array (or an array with only 1 element). Then assume it works
  28. >for any array with n-1 elements and from that prove that this implies
  29. >it also works for an array with n elements.
  30. >
  31. >Basically this idea is called mathematical induction. There is a weak and
  32. >strong form. I can't believe your teacher did not tell you about this
  33. >since that is obviously what is probably intended.
  34.  
  35. To expand on this, the invariant that Jason Klinke asked for is
  36. essentially the induction hypothesis.  If you are assuming that n > 0,
  37. this invariant works (sorry about the ASCII notation):
  38.  
  39.               _ i - 1
  40.     sum = >        A[j]    /\  (0 <= i <= n)
  41.           - j = 0
  42.  
  43. If you can't assume that n > 0, this invariant works:
  44.  
  45.               _ i - 1
  46.     sum = >        A[j]    /\  (0 <= i <= max(0, n))
  47.           - j = 0
  48.  
  49. My company has developed the Penelope verification system for proving
  50. the correctness of Ada programs, so just for fun I translated the loop
  51. to Ada and verified it under both assumptions.  (Because the semantics
  52. of C and Ada for loops is different, I rewrote the for loop as a while
  53. loop.)  Here's the program text under the assumption that n > 0:
  54.  
  55. --------------------------------- [Cut here] ---------------------------------
  56. with p;
  57. --| with trait t ;
  58. procedure foo(a : in p.intarray; n : in integer; sum : in out integer)
  59.   --| where
  60.   --|      in n>0;
  61.   --|      out sum = sigma(0, n-1, a);
  62.   --| end where;
  63.   --! VC Status: proved
  64.   --! BY instantiation of sigma_base as rewrite rule
  65.   --! BY limited simplification, simplification
  66.   --! BY synthesis of TRUE
  67.  
  68.  
  69. is
  70.   --! PRECONDITION = (0 = sigma(0, -1, a) and 0 <= n)
  71.   i : integer := 0;
  72.  
  73. begin
  74.   sum := 0;
  75.   --! PRECONDITION = (sum = sigma(0, i - 1, a) and (0 <= i and i <= n))
  76.   --! VC Status: proved
  77.   --! BY instantiation of sigma_step with (a for a, i for n)
  78.   --! rewriting left to right
  79.   --! BY simplification
  80.   --! BY synthesis of TRUE
  81.  
  82.   while (i<n) loop
  83.     --| invariant  sum = sigma(0, i-1, a) and (0<=i and i<=n);
  84.     sum := sum+a(i);
  85.     i := i+1;
  86.    end loop;
  87. end foo;
  88. -- 
  89. Douglas Harper    | 1976: lounge lizard
  90. +1 (607) 277-2020 | 1986: couch potato
  91. cdh@oracorp.com   | 1996: monitor lizard        (term swiped from Arden Tohill)
  92.